E:Type, pred?:(E(E+Unit)), e:E. first(e)  pred(e)  E 

latex

Definitions	P  Q, P & Q, Dec(P), P  Q, False, first(e), pred(e), outl(x), P  Q, A, b, b, isl(x), x:A. B(x), Unit, t  T
Lemmas	unit wf, isl wf, bnot wf, assert wf, not wf, outl wf, decidable assert, assert of bnot, not functionality wrt iff